guarded\_permutation($T$;$P$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$($\lambda$$L_{1}$,$L_{2}$. $\exists$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{1}$$\parallel-$1}}$. $P$($L_{1}$,$i$) \& $L_{2}$ $=$ swap($L_{1}$;$i$;$i$+1))$^{\mbox{\scriptsize $\ast$}}$